package soko.control;

import java.util.ArrayList;
import net.sf.javabdd.BDD;
import net.sf.javabdd.BDDFactory;
import net.sf.javabdd.BDDPairing;
import soko.sokoban.Direction;
import soko.sokoban.Tile;
import soko.sokoban.Tiles;

/**
 * A class that can solve sokoban puzzels using BDD's
 * @author Jeroen & Ruud
 */
public class Solver {

	Tiles tiles;
	BDDFactory factory;
	private boolean removeDeadlocks;
	private boolean countAllStates;
	private ArrayList<BDD> history = new ArrayList<BDD>();
	private BDD reverseRelation = null;
	private BDDPairing pairing = null;
	private BDD relation = null;
	private BDD[] directedRelations = null;
	
	/**
	 * Enumeration to distinguish variable kinds
	 * Used to determine veriable numbers
	 */
	public enum VarKind {
		BLOCK, MAN, MAN_TEMP, BLOCK_TEMP;
	}

	/**
	 * 
	 * @param tiles the tiles representation of the board
	 */
	public Solver(Tiles tiles) {
		this.tiles = tiles;
	}

	/**
	 * Returns the solution of the Sokoban puzzle or null if no solution was found.
	 * If counAllStates is true, it will return the empty string.
	 * @param findDeadlock false for normal solve, true to find the first deadlock state
	 * @param removeDeadlocks true to remove deadlock states, false for no deadlock detection
	 * @param countAllStates true to count all possible states and solutions
	 * @param lurd null or empty to not apply a lurd string to the initial state, or a string consisting of
	 * only l u r and d characters to apply a lurd string to the initial state
	 */
	public String getSolution(boolean findDeadlock, boolean removeDeadlocks, boolean countAllStates, String lurd){
		init();
		this.removeDeadlocks = removeDeadlocks;
		this.countAllStates = countAllStates;
		BDD initialState = getStateAfterLurd(lurd);
		//if getStateAfterLurd returned null, the lurd lead to a false or deadlock state
		//or the lurd string itself was false
		if(initialState == null) return null;
		if(countAllStates){
			//findDeadlock may not be true
			solve(false, initialState);
			return "";
		} else 
		if(solve(findDeadlock, initialState)) {
			return getLurd(findDeadlock);
		} else {
			return null;
		}
	}
	
	/**
	 * Returns state after applying the lurd argument to the initial state.
	 * If lurd is null or empty it will return the inital state.
	 * @param lurd a lurd string
	 * @return a BDD representing one state
	 */
	private BDD getStateAfterLurd(String lurd){
		BDD result = getInitialState();
		if(lurd != null && !lurd.isEmpty()){
			lurd = lurd.toLowerCase();
			if(!lurd.replaceAll("[lurd]", "").isEmpty()){
				System.err.println("Invalid lurd string: " +lurd);
				return null;
			}
			for(int i=0;i<lurd.length();i++){
				char lurdchar = lurd.charAt(i);
				switch(lurdchar){
				case 'l':
					result = applyRelation(result, Direction.LEFT);
					break;
				case 'u':
					result = applyRelation(result, Direction.UP);
					break;
				case 'r':
					result = applyRelation(result, Direction.RIGHT);
					break;
				case 'd':
					result = applyRelation(result, Direction.DOWN);
					break;
				default:
					throw new RuntimeException("Error in processing character '" + lurdchar + "' in lurd String: " + lurd);
					//it should not be possible that this happens
				}
				if(result.isZero()){
					System.err.println("The move in the lurd string at character " + (i+1) + " (" + lurdchar
							+") caused the man to walk off the board");
					return null;
				}
				if(removeDeadlocks){
					removeDeadlocks(result);
					if(result.isZero()){
						System.err.println("The move in the lurd string at character " + (i+1) + " (" + lurdchar
								+") caused a deadlock state.");
						return null;
					}
				}
			}
		}
		
		return result;
	}
	
	/**
	 * Initializes the BDD factory and then initializes all bdd's for future use
	 */
	public void init() {
		int numberOfNodes = 10000000;
		int cacheSize = 200000;
		factory = BDDFactory.init(numberOfNodes, cacheSize);

		factory.setVarNum(tiles.size() * 4);
		
		initRelations();

	}
	
	/**
	 * 
	 * @return the initial state as represented by Tiles
	 */
	private BDD getInitialState() {
		BDD result = factory.one();
		int position = tiles.getMan().getPosition();
		for (int i = 0; i < tiles.size(); i++) {
			result.andWith(getVar(VarKind.MAN, i, position != i));
			result.andWith(getVar(VarKind.BLOCK, i, !tiles.get(i).isBlock()));
		}
		return result;
	}
	
	/**
	 * 
	 * @param findDeadlock false for normal solve, true to find the first deadlock state
	 */
	private boolean solve(boolean findDeadlock, BDD initialState){
		if(findDeadlock)return solveFirstDeadlockState(initialState);
		else return solve(initialState);
	}
	
	/**
	 * Finds the first state that is recognised as a deadlock state
	 * @param initialState the state(s) to start searching from
	 * @return true if a solution was found, false if there is no deadlock state in the statespace
	 */
	private boolean solveFirstDeadlockState(BDD initialState){
		BDD states = initialState;
		history.add(states.id());
		boolean done = false;
		int iterationNumber = 0;
		while (!done) {
			BDD relationInput = states.id();
			BDD newStates = states.or(applyRelation(relationInput));
			iterationNumber++;
			System.err.println("Move: " + iterationNumber + " - States: " + newStates.pathCount());

			if (states.equals(newStates)) {
				//Greatest fixpoint reached, no solution
				break;
			} else {
				history.add(newStates.id().andWith(states.not()));
			}
			BDD result = newStates.id();
			removeNonDeadlocks(result);
			
			if (result.satCount(getManVars()) > 0) {
				done = true;

			}
			states.free();
			states = newStates;
		}
		
		return done;
	}
	
	/**
	 * Attempts to solve the sokoban puzzle, find the first state that is a solution
	 * If countAllStates, it will continue searching till the greatest fixpoint has been reached
	 * and report the numer of goal states.
	 * @param initialState
	 * @return
	 */
	private boolean solve(BDD initialState) {
		if(removeDeadlocks) removeDeadlocks(relation);
		BDD states = initialState;
		history.add(states.id());
		boolean done = false;
		int iterationNumber = 0;
		while (!done) {
			BDD relationInput = states.id();
			BDD newStates = states.or(applyRelation(relationInput));
			iterationNumber++;
			System.err.println("Move: " + iterationNumber + " - States:" + newStates.pathCount());

			if (states.equals(newStates)) {
				//Greatest fixpoint reached, no solution (or ready to count goalstates)
				if(countAllStates){
					BDD result = newStates.and(getGoals());
					System.out.println("All states found, number of solutions: " + result.pathCount());
				}
				break;
			} else {
				history.add(newStates.id().andWith(states.not()));
			}
			BDD result = newStates.and(getGoals());
			
			if (result.satCount(getManVars()) > 0) {
				if(!countAllStates) done = true;

			}
			states.free();
			states = newStates;
		}
		
		return done;

	}
	
	/**
	 * Returns the lurdString of the solution that solve has found
	 * solve() should have been called first
	 * @param findDeadlock false for normal solve, true to find the first deadlock state
	 */
	private String getLurd(boolean findDeadlock) {
		if(findDeadlock){
			BDD bdd = history.get(history.size() - 1);
			removeNonDeadlocks(bdd);
			return getLurd(bdd);
		}
		else{
			return getLurd(history.get(history.size() - 1).and(getGoals()));
		}
	}
	
	/**
	 * Calculates the Lurd string for the result with current state as final state
	 * @param currentState The final state in the history
	 * @return a lurd String
	 */
	private String getLurd(BDD currentState) {
		String lurd = "";
		for (int i = history.size() - 2; i >= 0; i--) {
			BDD previousStates = history.get(i);

			BDD neighbourstates = currentState.relprod(reverseRelation, getManAndBlockVars());
			neighbourstates.replaceWith(pairing);
			previousStates.andWith(neighbourstates);

			for (Object sat : previousStates.allsat()) {
				byte[] bytes = (byte[]) sat;
				BDD possiblePrevState = byteArrayToBDD(bytes);
				BDD test = applyRelation(possiblePrevState, Direction.LEFT).and(currentState);
				if (!test.isZero()) {
					currentState = possiblePrevState;
					lurd = "l" + lurd;
					break;
				}
				test = applyRelation(possiblePrevState, Direction.UP).and(currentState);
				if (!test.isZero()) {
					currentState = possiblePrevState;
					lurd = "u" + lurd;
					break;
				}
				test = applyRelation(possiblePrevState, Direction.RIGHT).and(currentState);
				if (!test.isZero()) {
					currentState = possiblePrevState;
					lurd = "r" + lurd;
					break;
				}
				test = applyRelation(possiblePrevState, Direction.DOWN).and(currentState);
				if (!test.isZero()) {
					currentState = possiblePrevState;
					lurd = "d" + lurd;
					break;
				}
			}
		}

		return lurd;
	}

	/**
	 * Converts a byte array with variables to a BDD representing a single state
	 * @param vars the variables
	 * @return a BDD representing a single state
	 */
	private BDD byteArrayToBDD(byte[] vars) {
		BDD result = factory.one();

		for (int i = 0; i < tiles.size(); i++) {
			result.andWith(getVar(VarKind.MAN, i, vars[getVarNo(VarKind.MAN, i)] == 0));
			result.andWith(getVar(VarKind.BLOCK, i, vars[getVarNo(VarKind.BLOCK, i)] == 0));
		}

		return result;
	}
	
	/**
	 * @return a BDD with the goal state (there is a block on each goal and no block on every other spot)
	 */
	private BDD getGoals() {
		BDD result = factory.one();
		for (Tile tile : tiles) {
			result.andWith(getVar(VarKind.BLOCK, tile.getPosition(), !tile.isGoal()));
		}
		return result;
	}

	/**
	 * Applies the relation function tot the states argument
	 * @param a bdd representing one or more states
	 * @return A BDD representing the set of states that follow from the states argument
	 */
	private BDD applyRelation(BDD states) {
		BDD result = states.relprod(relation, getManAndBlockVars());
		result.replaceWith(pairing);
		return result;
	}
	
	/**
	 * Applies the relation function for one direction to the states argument
	 * @param states a bdd representing one or more states
	 * @param direction the direction in which the function should be applied
	 * @return A BDD representing the state or states that follow from the states argument
	 */
	private BDD applyRelation(BDD states, Direction direction) {
		BDD rel = getRelation(direction);
		BDD result = states.relprod(rel, getManAndBlockVars());
		result.replaceWith(pairing);
		return result;
	}

	/**
	 * Calculates the BDD that represents the next state function in one direction for the tile in the argument
	 * @param tile the tile to calculate the next state function fore
	 * @param direction the direction for the next state function
	 * @return a BDD that is a relation function for the Sokoban game
	 */
	private BDD nextState(Tile tile, Direction direction) {
		int curPosition = tile.getPosition();
		int nextPosition;
		int doubleNextPosition;

		Tile next = tile.getTile(direction);
		BDD result = factory.zero();
		if (next != null) {
			nextPosition = next.getPosition();
			result.xorWith(nextState(curPosition, nextPosition));
			//vervolgens kijken of als er een block voor de man staat, deze te verschuiven
			Tile doubleNext = next.getTile(direction);
			if (doubleNext != null) {
				doubleNextPosition = doubleNext.getPosition();
				result.xorWith(nextState(curPosition, nextPosition, doubleNextPosition));
			}
		}
		return result;
	}

	/**
	 * Calculates the next state function where the Man walks from curPosition to nextPosition
	 * @param curPosition the position of the man
	 * @param nextPosition the next position of the man
	 * @return the next state function for moving the man
	 */
	private BDD nextState(int curPosition, int nextPosition) {
		BDD nextState = getVar(VarKind.MAN, curPosition);
		nextState.andWith(getVar(VarKind.MAN_TEMP, nextPosition, false));
		nextState.andWith(getVar(VarKind.BLOCK, curPosition, true)); //no block on curposition
		nextState.andWith(getVar(VarKind.BLOCK, nextPosition, true)); //no block on nextposition

		for (int i = 0; i < tiles.size(); i++) {
			if (i != curPosition) {
				nextState.andWith(getVar(VarKind.MAN, i, true));
			}
			if (i != nextPosition) {
				nextState.andWith(getVar(VarKind.MAN_TEMP, i, true));
			}
			BDD blockBiImp = getVar(VarKind.BLOCK, i);
			blockBiImp.biimpWith(getVar(VarKind.BLOCK_TEMP, i));
			nextState.andWith(blockBiImp);
		}

		return nextState;
	}

	/**
	 * Calculates the next state where the man moves from curPosition to nextPosition and
	 * pushes a block from nextPosition to doubleNextPosition
	 * @param curPosition the current position of the man
	 * @param nextPosition the possible next position of the man (there may be a block here)
	 * @param doubleNextPosition the position after nextPosition (a block might be moved here)
	 * @return the next state function for moving a block for these positions
	 */
	private BDD nextState(int curPosition, int nextPosition, int doubleNextPosition) {
		BDD nextState = getVar(VarKind.MAN, curPosition); // man is on curposition
		nextState.andWith(getVar(VarKind.BLOCK, curPosition, true)); //no block on curposition
		nextState.andWith(getVar(VarKind.BLOCK, nextPosition, false)); //there is a block on nextPosition
		nextState.andWith(getVar(VarKind.BLOCK_TEMP, nextPosition, true)); //block no longer in nextposition
		nextState.andWith(getVar(VarKind.MAN_TEMP, nextPosition, false)); //the man moves to nextposition
		nextState.andWith(getVar(VarKind.BLOCK, doubleNextPosition, true)); //no block on doubleNextPosition
		nextState.andWith(getVar(VarKind.BLOCK_TEMP, doubleNextPosition, false)); //block moves to doubleNextPosition

		for (int i = 0; i < tiles.size(); i++) {
			if (i != curPosition) {
				nextState.andWith(getVar(VarKind.MAN, i, true));
			}
			if (i != nextPosition) {
				nextState.andWith(getVar(VarKind.MAN_TEMP, i, true));
			}

			if (i != nextPosition && i != doubleNextPosition) {
				BDD blockBiImp = getVar(VarKind.BLOCK, i);
				blockBiImp.biimpWith(getVar(VarKind.BLOCK_TEMP, i));
				nextState.andWith(blockBiImp);
			}
		}
		return nextState;
	}

	/**
	 * Calculate the previous state BDD relation function in the supplied direction
	 * @param tile
	 * @param direction the direction of the previousState The direction itself
	 * is not reversed by this method!
	 */
	private BDD previousState(Tile tile, Direction direction) {
		int curPosition = tile.getPosition();
		int nextPosition;
		int oppositePosition;

		Tile prev = tile.getTile(direction);
		BDD result = factory.zero();
		if (prev != null) {
			nextPosition = prev.getPosition();
			result.xorWith(previousState(curPosition, nextPosition)); //calculate prevstate1 (see example below)
			// next is moving blocks backwards
			// this is more complex:
			// currstate    prevstate1    prevstate2
			//  #####         #####         #####
			//  # @$#         #@ $#         #@$ #
			//  #####         #####         #####
			//
			// The example above is for Direction.LEFT, in prevstate1 (already calculated)
			// the man steps back to the left
			// in prevstate2 the man takes the block on his right side with him
			Tile opposite = tile.getTile(direction.getOpposite());
			if (opposite != null) {
				oppositePosition = opposite.getPosition();
				result.xorWith(previousState(curPosition, nextPosition, oppositePosition));
			}
		}
		return result;
	}

	/**
	 * Calculate the previous state BDD function for the two supplied positions
	 * @param curPosition the current position of the man
	 * @param prevPosition the position of the man in the previous state
	 * @return
	 */
	private BDD previousState(int curPosition, int prevPosition) {
		/*
		 * Even though the idea of the previous and next method is essentially
		 * different, this method returns the same result. This is because this
		 * is a base case where the man does not move any blocks. Moving forwards
		 * is exactly the same as moving backwards in this case.
		 */
		return nextState(curPosition, prevPosition);
	}
	
	/**
	 * Calculate the previous state bdd function
	 * In this case the man moves (back) to prevPosition and pulls the block from oppositePosition to curPosition
	 * @param curPosition the current position of the man
	 * @param prevPosition the position of the man in a possible previous state
	 * @param oppositePosition the position at the other side of the man (there may be a block here)
	 */
	private BDD previousState(int curPosition, int prevPosition, int oppositePosition) {

		BDD result = getVar(VarKind.MAN, curPosition); // man staat op curPosition
		result.andWith(getVar(VarKind.BLOCK, curPosition, true)); //geen block op curPosition
		result.andWith(getVar(VarKind.BLOCK_TEMP, curPosition, false)); //block verplaatst naar curPosition

		result.andWith(getVar(VarKind.BLOCK, prevPosition, true)); //er staat geen block op nextPosition
		result.andWith(getVar(VarKind.MAN_TEMP, prevPosition, false)); //verplaatsing van man
		result.andWith(getVar(VarKind.BLOCK, oppositePosition, false)); //block op oppositePosition
		result.andWith(getVar(VarKind.BLOCK_TEMP, oppositePosition, true)); //geen block meer op oppositePosition

		for (int i = 0; i < tiles.size(); i++) {
			if (i != curPosition) {
				result.andWith(getVar(VarKind.MAN, i, true));
			}
			if (i != prevPosition) {
				result.andWith(getVar(VarKind.MAN_TEMP, i, true));
			}

			if (i != curPosition && i != oppositePosition) {
				BDD blockBiImp = getVar(VarKind.BLOCK, i);
				blockBiImp.biimpWith(getVar(VarKind.BLOCK_TEMP, i));
				result.andWith(blockBiImp);
			}
		}
		return result;
	}
	
	/**
	 * Returns a BDD with all variables related to the man must be true for the BDD to be true
	 * (Required for the relprod function)
	 */
	private BDD getManVars() {
		BDD var = factory.one();
		for (int i = 0; i < tiles.size(); i++) {
			var.andWith(getVar(VarKind.MAN, i));
		}
		return var;
	}

	/**
	 * Returns a BDD with all variables related to block must be true for the BDD to be true
	 * (Required for the relprod function)
	 */
	private BDD getBlockVars() {
		BDD var = factory.one();
		for (int i = 0; i < tiles.size(); i++) {
			var.andWith(getVar(VarKind.BLOCK, i));
		}
		return var;
	}

	/**
	 * Returns a BDD with all varibles related to the man or blocks true for the bdd to be true
	 * (Required for the relational product)
	 */
	private BDD getManAndBlockVars() {
		return getManVars().andWith(getBlockVars());
	}
	
	/**
	 * Returns the varibale number used in the BDD's
	 * @param kind varible kind
	 * @param number number of the tile
	 */
	private int getVarNo(VarKind kind, int number) {
		int varnum = -1;
		switch (kind) {
			case MAN:
				varnum = number;
				break;
			case MAN_TEMP:
				varnum = number + tiles.size();
				break;
			case BLOCK:
				varnum = number * 2 + tiles.size() * 2;
				break;
			case BLOCK_TEMP:
				varnum = number * 2 + 1 + tiles.size() * 2;
				break;
			default:
				throw new RuntimeException("Invalid varkind: " + kind);
		}
		return varnum;
	}
	
	/**
	 * Returns a BDD representing one varibale the true (high) child points to true;
	 * @param kind varible kind
	 * @param number number of the tile
	 */
	private BDD getVar(VarKind kind, int number) {
		return getVar(kind, number, false);
	}
	
	/**
	 * Returns a BDD representing one varibale the true (high) child points to true
	 * when inverse is true, the true branch points to false
	 * @param kind varible kind
	 * @param number number of the tile
	 * @param inverse invert if the false (low) child should point to true
	 */
	private BDD getVar(VarKind kind, int number, boolean inverse) {
		int varnum = getVarNo(kind, number);
		if (inverse) {
			return factory.nithVar(varnum);
		} else {
			return factory.ithVar(varnum);
		}
	}
	
	/**
	 * returns the relation for one specific direction
	 * @param direction
	 */
	private BDD getRelation(Direction direction) {
		switch (direction) {
			case LEFT:
				return directedRelations[0];
			case UP:
				return directedRelations[1];
			case RIGHT:
				return directedRelations[2];
			case DOWN:
				return directedRelations[3];
		}
		return null; //can not happen unless direction is null
	}

	//////////////////////////////
	////////INIT FUNCTIONS////////
	//////////////////////////////
	
	/**
	 * Initializes the reverse relation function (for moving backwards)
	 */
	private void initReverseRelation(){
		if (reverseRelation == null) {
			reverseRelation = factory.zero();
			for (Tile tile : tiles) {
				// 4 directions
				reverseRelation.xorWith(previousState(tile, Direction.LEFT));
				reverseRelation.xorWith(previousState(tile, Direction.UP));
				reverseRelation.xorWith(previousState(tile, Direction.RIGHT));
				reverseRelation.xorWith(previousState(tile, Direction.DOWN));
			}
		}
	}

	/**
	 * Initializes the BDD pairing
	 */
	private void initPairing() {
		if (pairing == null) {
			pairing = factory.makePair();
			for (int i = 0; i < tiles.size(); i++) {
				pairing.set(getVarNo(VarKind.MAN_TEMP, i), getVarNo(VarKind.MAN, i));
				pairing.set(getVarNo(VarKind.BLOCK_TEMP, i), getVarNo(VarKind.BLOCK, i));
			}
		}
	}

	/**
	 * Initializes the relation (tranistion) function
	 */
	private void initRelation() {
		if (relation == null) {
			relation = factory.zero();
			for (Tile tile : tiles) {
				// 4 directions
				relation.xorWith(nextState(tile, Direction.LEFT));
				relation.xorWith(nextState(tile, Direction.UP));
				relation.xorWith(nextState(tile, Direction.RIGHT));
				relation.xorWith(nextState(tile, Direction.DOWN));
			}
		}
	}
	
	/**
	 * Initializes the relation (tranistion) function for the four direction seperately
	 */
	private void initDirectedRelation() {
		if (directedRelations == null) {
			directedRelations = new BDD[4];
			for (Direction direction : Direction.values()) {
				BDD result = factory.zero();
				for (Tile tile : tiles) {
					// 1 direction
					result.xorWith(nextState(tile, direction));
				}
				switch (direction) {
					case LEFT:
						directedRelations[0] = result;
						break;
					case UP:
						directedRelations[1] = result;
						break;
					case RIGHT:
						directedRelations[2] = result;
						break;
					case DOWN:
						directedRelations[3] = result;
						break;
				}
			}
		}
	}

	/**
	 * Calls all functions that initialize BDD's
	 */
	private void initRelations() {
		initReverseRelation();
		initDirectedRelation();
		initRelation();
		initPairing();
		initNonDeadLockStates();
		
	}
	
		//////////////////////////////
		//////DEADLOCK FUNCTIONS//////
		//////////////////////////////
	private BDD nonDeadBlockPositions;
	private BDD nonDeadCorridorStates;
	private BDD simpleNonBiparitieDeadlockPositions;
	private BDD notImmovableBlocksStates;
	
	/**
	 * Initializes all non deadlock state BDD's
	 */
	private void initNonDeadLockStates(){
		System.err.println("Generating deadlock states");
		nonDeadBlockPositions = getNonDeadLockBlockPositions();
		nonDeadCorridorStates =getNonDeadCorridorStates();
		simpleNonBiparitieDeadlockPositions=getSimpleNonBiparitieDeadlockPositions();
		notImmovableBlocksStates=getNotImmovableBlocksStates();
		System.err.println("Finished generating deadlock states");
	}
	
	/**
	 * Removes all deadlock states from a BDD
	 */
	private void removeDeadlocks(BDD bdd){
		bdd.andWith(nonDeadBlockPositions.id());
		bdd.andWith(nonDeadCorridorStates.id());
		bdd.andWith(simpleNonBiparitieDeadlockPositions.id());
		bdd.andWith(notImmovableBlocksStates.id());
	}
	
	/**
	 * Removes all non deadlock states from a BDD
	 */
	private void removeNonDeadlocks(BDD bdd){
		BDD deadlocks = nonDeadBlockPositions.id();
		deadlocks.andWith(nonDeadCorridorStates.id());
		deadlocks.andWith(simpleNonBiparitieDeadlockPositions.id());
		deadlocks.andWith(notImmovableBlocksStates.id());
		bdd.andWith(deadlocks.not());
	}	
	
	/**
	 * Return states where no combination of blocks and walls cause
	 * blocks to become immovable.
	 * This algorithm does not detect all states where blocks are immovable.
	 */
	private BDD getNotImmovableBlocksStates(){
		BDD result = factory.one();
		Tile a,b,c;
		for(Tile current : tiles){
			/*
			 * Check for 4 bock square situation:
			 * (at least one must not be a goal)
			 * Example:
			 * $$
			 * $$
			 */
			a = current.getDownTile();
			b = current.getRightTile();
			c = b == null? null : b.getDownTile();
			excludeImpossibleBlockPosition(current, a, b, c, 0, result);
			
			/*
			 * Check for 3 bock and 1 wall square situation:
			 * (at least one must not be a goal)
			 * Situations:
			 * #$ or $#  or $$  or $$
			 * $$    $$     #$     $#
			 * We check for all four
			 */
			a = current.getRightTile();
			b = a == null? null : a.getUpTile();
			c = current.getUpTile(); //must be a wall
			excludeImpossibleBlockPosition(current, a, b, c, 1, result);
			
			a = current.getDownTile();
			b = a == null? null : a.getRightTile();
			c = current.getRightTile(); //must be a wall
			excludeImpossibleBlockPosition(current, a, b, c, 1, result);
			
			a = current.getRightTile();
			b = a == null? null : a.getDownTile();
			c = current.getDownTile(); //must be a wall
			excludeImpossibleBlockPosition(current, a, b, c, 1, result);
			
			a = current.getLeftTile();
			b = a == null? null : a.getDownTile();
			c = current.getDownTile(); //must be a wall
			excludeImpossibleBlockPosition(current, a, b, c, 1, result);
			
			/*
			 * Check for 2 bock and 2 wall square situation:
			 * (at least one must not be a goal)
			 * Situations:
			 * #$ or $#  or ##  or $$
			 * #$    $#     $$     ##
			 * We check for all four
			 * Note that the deadlock situations where the walls are diagonal
			 * are already recognised by the getNonDeadLockBlockPositions() method
			 */
			a = current.getDownTile();
			b = a == null? null : a.getLeftTile(); //must be a wall
			c = current.getLeftTile(); //must be a wall
			excludeImpossibleBlockPosition(current, a, b, c, 2, result);
			
			a = current.getDownTile();
			b = a == null? null : a.getRightTile(); //must be a wall
			c = current.getRightTile(); //must be a wall
			excludeImpossibleBlockPosition(current, a, b, c, 2, result);
			
			a = current.getRightTile();
			b = a == null? null : a.getDownTile(); //must be a wall
			c = current.getDownTile(); //must be a wall
			excludeImpossibleBlockPosition(current, a, b, c, 2, result);
			
			a = current.getRightTile();
			b = a == null? null : a.getUpTile(); //must be a wall
			c = current.getUpTile(); //must be a wall
			excludeImpossibleBlockPosition(current, a, b, c, 2, result);
			
			/*
			 * Check for 2 bock and 2 wall tetris block situation:
			 * (at least one must not be a goal)
			 * Situations:
			 * #$ or  $#  or #  or   #
			 *  $#   #$      $$     $$
			 *                #     #
			 * We check for all four
			 * Current is the upper or leftmost block
			 */
			a = current.getDownTile();
			b = a == null? null : a.getRightTile(); //must be a wall
			c = current.getLeftTile(); //must be a wall
			excludeImpossibleBlockPosition(current, a, b, c, 2, result);
			
			a = current.getDownTile();
			b = a == null? null : a.getLeftTile(); //must be a wall
			c = current.getRightTile(); //must be a wall
			excludeImpossibleBlockPosition(current, a, b, c, 2, result);
			
			a = current.getRightTile();
			b = a == null? null : a.getDownTile(); //must be a wall
			c = current.getUpTile(); //must be a wall
			excludeImpossibleBlockPosition(current, a, b, c, 2, result);
			
			a = current.getRightTile();
			b = a == null? null : a.getUpTile(); //must be a wall
			c = current.getDownTile(); //must be a wall
			excludeImpossibleBlockPosition(current, a, b, c, 2, result);
			
		}
		return result;
	}
	
	/**
	 * help method for getNotImmovableBlocksStates()
	 * @param current first tile for deadlock state check
	 * @param a other tile for deadlock state check
	 * @param b other tile for deadlock state check or a possible wall (null) if numwalls == 2
	 * @param c other tile for deadlock state check or a possible wall if numwalls == 1  or 2
	 * @param numwalls number of walls
	 * @param andWith the BDD to AND the result with (since there is no return value
	 */
	private void excludeImpossibleBlockPosition(Tile current, Tile a, Tile b,
			Tile c, int numwalls, BDD andWith) {
		switch (numwalls) {
		case 0:
			if (a != null && b != null && c != null && !(current.isGoal()
					&& a.isGoal() && b.isGoal() && c.isGoal())) {
				BDD toAdd = getVar(VarKind.BLOCK, current.getPosition());
				toAdd.andWith(getVar(VarKind.BLOCK, a.getPosition()));
				toAdd.andWith(getVar(VarKind.BLOCK, b.getPosition()));
				toAdd.andWith(getVar(VarKind.BLOCK, c.getPosition()));
				andWith.andWith(toAdd.not());
			}
			break;
		case 1:
			if (a != null && b != null && c == null && !(current.isGoal()
					&& a.isGoal() && b.isGoal())) {
				BDD toAdd = getVar(VarKind.BLOCK, current.getPosition());
				toAdd.andWith(getVar(VarKind.BLOCK, a.getPosition()));
				toAdd.andWith(getVar(VarKind.BLOCK, b.getPosition()));
				
				andWith.andWith(toAdd.not());
			}
			break;
		case 2:
			if (a != null && b == null && c == null && !(current.isGoal()
					&& a.isGoal())) {
				BDD toAdd = getVar(VarKind.BLOCK, current.getPosition());
				toAdd.andWith(getVar(VarKind.BLOCK, a.getPosition()));
				
				andWith.andWith(toAdd.not());
			}
			break;
		}
	}
	
	/**
	 * Dead corridor detection.
	 * Some squares are deadlock squares because pushing a box to them ends
	 * in a one way street. Example:<pre>
	 *     ####
	 * #####  #
	 * #DDDD  #    D = dead end squares which are deadlock squares  
	 * #####$ # 
	 *     #+ #
	 *     ####</pre>
	 * 
	 * There must be no goal in the corridor, and if the man
	 * starting position is in the corridor then only the position
	 * of the man, and those deeper in the corridor are deadlock positions
	 * @return a BDD with all states where there is no block in a dead Corridor
	 */
	private BDD getNonDeadCorridorStates(){
		BDD result = factory.one();
		
		boolean[] corridor = new boolean[tiles.size()];
		for(Tile t : tiles){
			if(!t.isGoal()){
				int wallCount =0;
				if(t.getLeftTile() == null) wallCount++;
				if(t.getRightTile() == null) wallCount++;
				if(t.getUpTile() == null) wallCount++;
				if(t.getDownTile() == null) wallCount++;
				if(wallCount == 3){
					if(t.getLeftTile() != null) expandCorridor(corridor, t, Direction.LEFT);
					else if(t.getUpTile() != null) expandCorridor(corridor, t, Direction.UP);
					else if(t.getRightTile() != null) expandCorridor(corridor, t, Direction.RIGHT);
					else if(t.getDownTile() != null) expandCorridor(corridor, t, Direction.DOWN);
				}
			}
		}
		
		for(int i=0; i< tiles.size();i++){
			if(corridor[i]){
				result.andWith(getVar(VarKind.BLOCK, i, true));
			}
		}
		return result;
	}
	
	/**
	 * Help method for getNonDeadCorridorStates
	 * @param corridor an array with corridor positions set to true
	 * @param t the new corridor tile
	 * @param direction the direction in which to the corridor is open
	 */
	private void expandCorridor(boolean[] corridor, Tile t, Direction direction){
		corridor[t.getPosition()] = true;
		Tile next = t.getTile(direction);
		//stop if the man started at t or if the next is a goal
		if(!t.isMan() && next != null && !next.isGoal()){
			int wallCount=0;
			for(Direction d : Direction.values()){
				if(d != direction && d != direction.getOpposite()){
					if(next.getTile(d) == null){
						wallCount++;
					}
				}
				if(wallCount ==2){
					expandCorridor(corridor, next, direction);
				}
			}
		}
	}
	
	/**
	 * Returns a BDD in which all the tiles where a block can never
	 * reach any goal are false
	 * Example: the tiles marked x may never have blocks in them
	 *    #####
	 *    #xxx#
	 *    #$$$#
	 * ####   #
	 * #x  .#$##
	 * #x$.$. .#
	 * #xx#.#.##
	 * ########
	 */
	private BDD getNonDeadLockBlockPositions(){
		BDD result = factory.one();
		
		boolean[] reachable = new boolean[tiles.size()];
		
		for(Tile tile : tiles){
			if(tile.isGoal()){
				expandReachableArray(reachable, tile);
			}
		}
		
		for(int i=0; i< tiles.size();i++){
			if(!reachable[i]){
				result.andWith(getVar(VarKind.BLOCK, i, true));
			}
		}
		
		return result;
	}
	
	/**
	 * Detect Simple bipartite deadlocks. These are sets of squares
	 * on which there must be at leas one block. Else it is not possible
	 * that a block will ever reach one of the goals.
	 * Example:<pre>
	 *   ######
	 *   #.$ @#
	 *   ## x.#
	 *    #   #
	 *    #####</pre>
	 * 
	 * For the right goal, there must be a block either on the goal, or on the
	 * position marked x. In any other case, it is not possible to push a block
	 * into this goal. This algorithm will check for each goal if there is a block
	 * in the set of positions from which a block can be pushed into that goal.
	 * @return a bdd where all states have no simple biparite deadlocks
	 */
	private BDD getSimpleNonBiparitieDeadlockPositions(){
		BDD result = factory.one();
		
		boolean[] reachable;
		
		for(Tile tile : tiles){
			if(tile.isGoal()){
				BDD goalRequirements = factory.zero();
				reachable = new boolean[tiles.size()];
				expandReachableArray(reachable, tile);
				for(int i=0; i< tiles.size();i++){
					if(reachable[i]){
						goalRequirements.orWith(getVar(VarKind.BLOCK, i));
					}					
				}
				result.andWith(goalRequirements);
			}
		}
		return result;
	}
	
	/**
	 * help method for getSimpleNonBiparitieDeadlockPositions()
	 * @param array a boolean array with positions from which blocks can reach a goal set to true
	 * @param newTile the new tile that should be set to true (and from which the algorithm will expand)
	 */
	private void expandReachableArray(boolean[] array, Tile newTile){
		if(!array[newTile.getPosition()]){
			array[newTile.getPosition()] = true;
			//if there are two walkable positions left of the tile
			if(newTile.getLeftTile() != null && newTile.getLeftTile().getLeftTile() != null){
				expandReachableArray(array, newTile.getLeftTile());
			}
			//if there are two walkable positions above the tile
			if(newTile.getUpTile() != null && newTile.getUpTile().getUpTile() != null){
				expandReachableArray(array, newTile.getUpTile());
			}
			//if there are two walkable positions right of the tile
			if(newTile.getRightTile() != null && newTile.getRightTile().getRightTile() != null){
				expandReachableArray(array, newTile.getRightTile());
			}
			//if there are two walkable positions under the tile
			if(newTile.getDownTile() != null && newTile.getDownTile().getDownTile() != null){
				expandReachableArray(array, newTile.getDownTile());
			}
		}
	}
}